Verification of computerized systems, such as circuits, chips, or other hardware components is an important part of the quality assurance process. A design of the system may be verified. The design may be provided in a manner defining its functionality, such as using Verilog, Hardware Description Language (HDL), or the like.
Verification techniques include simulation of stimuli to the design, which may be performed using a software simulator, emulator, hardware accelerator, or the like. Simulation may be performed based on the design. Simulation may be purely random, heuristically guided, or the like. During simulation, certain conditions or assertions, also referred to as checkers, may be checked. Checkers may be defined using Property Specification Language (PSL) or other languages. In case, the condition is met or the assertion is violated, the simulation may provide the simulated trace exemplifying such an occurrence.
Another verification technique is formal verification during which the design is formally proven to hold a specification property (e.g., AGp property, EFp property, or the like). In case the design does not hold the specification property, a counter-example is provided showing a particular trace in which the design does not hold the property. There are several formal verification techniques, such as but not limited to model checking, theorem proving, equivalence checking, or the like.
Yet another verification technique is semi-formal verification in which formal and non-formal methods are combined. Semi-formal verification may leverage formal algorithms without unlimited resources and may be used to find bugs too complex or deep for pure formal search. One example of semi-formal verification method is symbolic execution in which a group of executions are symbolically represented by a single simulated execution. Another example of semi-formal verification includes iterating between simulation and formal algorithms.
In the present disclosure, all examined properties, be them specification properties, assertions, or the like, are commonly referred to as properties. The present disclosure generally refers to the properties as being checked by checkers.
It is not rare that a verification engineer verifies, using formal, non-formal or semi-formal technique, a design and discovers bugs in the design. The bug may be exemplified in a trace of the design. After the bugs are found, the design may be manually modified, such as by a designer, to correct the design, fix the bug, or the like. However, after the design is modified, it may be desired to verify the modified design as well.